L:MsgA List, l:IdLnk, tg:Id.
(A,BL.A ||+ B)
 (rcv(l,tg) declared in (L)  reduce(M,x. rcv(l,tg)  dom(1of(2of(M)))  x;false;L)) 

latex

Definitions	(L), false, P  Q, P  Q, P & Q, False, reduce(f;k;as), p  q, , x  dom(f), KindDeq, rcv(l,tg), 1of(t), P  Q, {T}, a:A fp B(a), x. t(x), Knd, rcv(l,tg) declared in M, Valtype(da;k), (xL.P(x)), b, IdLnk, Id, (x,yL.P(x;y)), x,y. t(x;y), MsgA, Prop, A ||+ B, x:A. B(x), t  T, P  Q
Lemmas	ma-compat wf, msga wf, pairwise wf, Id wf, IdLnk wf, ma-join-list-declm, Knd wf, fpf-trivial-subtype-top, ma-declm wf, l exists wf, rcv wf, Kind-deq wf, fpf-dom wf, assert wf, bool wf, bor wf, reduce wf, assert of bor, l exists cons, l exists nil, bfalse wf, ma-join-list wf